Restart method and exponential acceleration of random 3-SAT instances resolutions: a large deviation analysis of the Davis-Putnam-Loveland-Logemann algorithm

摘要

The analysis of the solving complexity of random 3-SAT instances using theDavis-Putnam-Loveland-Logemann (DPLL) algorithm slightly below threshold ispresented. While finding a solution for such instances demands exponentialeffort with high probability, we show that an exponentially small fraction ofresolutions require a computation scaling linearly in the size of the instanceonly. We compute analytically this exponentially small probability of easyresolutions from a large deviation analysis of DPLL with the Generalized UnitClause search heuristic, and show that the corresponding exponent is smaller(in absolute value) than the growth exponent of the typical resolution time.Our study therefore gives some quantitative basis to heuristic restart solvingprocedures, and suggests a natural cut-off cost (the size of the instance) forthe restart.